\section{Introduction}
\label{sec:intro}

Smart-cards are ubiquitous and are universally considered to be
secure, tamper-proof, and trustworthy devices. They have been used to
implement confidential operations such as user identification and
authentication and sensitive data storage and processing. These
operations involve a deliberately confidential communication between
smart-cards and third-party systems. Such communication is prone
to ``man-in-the-middle'' attacks thus rendering smart-cards
vulnerable.

\comment{ Sniffing the smart-card communication and consequently
  perform man-in-the-middle attacks has attracted a lot of attention
  and many tools have been proposed (\eg
  \cite{detective,smartlogig-koning}). Studies have exposed that such
  attacks reveal severe problems. For example, by blind-replaying a
  communication session one may distinguish different
  passports~\cite{epassports}. An attack may vary depending on the
  target: knowledge of the semantics of a communication session may
  suggest attacks like the previous one, or PIN or authentication data
  linkage, or may imply access to the card to execute unauthorised
  operations. However, for an attack to be universally successful it
  has to deal with proprietary protocol implementations as well as
  with inter-industry ones, an issue that previous studies do not
  address.}{why reverse-engineering APDUs}

\comment{Attacking and fixing cryptographic standards used by
  smart-cards, such as RSA PKCS\#11, is an active area. As defined in
  PKCS\#11~\cite{pkcs}, cryptography is only one aspect of security
  and the token is only one component in a system; one must consider
  the environment the token operates in as well. Smart-cards
  supposedly offer a tamper-proof environment for protecting sensitive
  data, but should also be designed so that this data remains secure.
  This is delegated to the communication protocols, under the
  assumption that these protocols are secure. Proprietary
  implementations create the illusion of security as they hide the
  card's code. A smart-card operates as a black-box: only access to
  the card's code may reveal the semantics of the communication
  protocol and its internal operations. We propose
  reverse-engineering the smart-card communication protocol, with
  respect to PKCS\#11, to determine the security of that
  implementation. We present REPROVE, which stands for Reverse
  Engineering of PROtocols for VErification: an automated tool, that
  infers the semantics of the communication, the on-card operations
  and their interconnection with the PKCS\#11. REPROVE is
  implementation- and function-independent, as it deals with both
  inter-industry and proprietary implementations and does not require
  access to the card's code. }{why reverse-engineer APDU with respect
  a crypto standard like PKSCS11}

RSA PKCS\#11 defines an Application Programming Interface (API) for
smart-cards. Any high-level interaction (\eg to obtain data from a
smart-card) generates a communication trace that corresponds to a
series of API calls by the smart-card/host. REPROVE reverse-engineers
the low-level implementation of the cryptographic protocol by
automatically aligning the byte-wise decomposition of the
communication trace to expected RSA PKCS\#11 calls for specific types
of functionality. This process is helpful in multiple ways:
\begin{inparaenum}[(\itshape a\upshape)]
\item It provides the means to   test smart-card implementations
  and discover their security vulnerabilities.
\item In the absence of detected vulnerabilities, it provides
  %additional 
  empirical evidence for the security of the
  implementation.
\item It can be used by the developers of smart-card technologies to
  test %and reason about 
  their implementations.
\item It can be used by the clients themselves, to test whether
  their card %is secure or it 
  is vulnerable to attack and,
  therefore, fraud.
\end{inparaenum}
\comment{An alternative to REPROVE's automated reasoning is to
  manually reverse-engineer the trace. This is not straightforward and
  is far from a quick exercise. It requires access to the card's
  library and its internal calls, whereas REPROVE does not. If one
  tries to \textit{guess} the meaning of the trace, without access to
  the card, then, given the combinatorial nature of the problem, one
  will need to test a considerably large number of combinations (\eg
  in some of the cards we tested there are 81881 combinations---see
  also Section~\ref{sec:results:number}) which will require a long
  time to decode. REPROVE does this in a matter of minutes.}{REPROVE
  vs manually reverse-engineering (reviewer's comment )}

A security token, such as a smart-card, implements all the
cryptographic operations internally. The token stores objects (\eg
data and certificates) that can be accessed via session handles, and
performs cryptographic functions. RSA PKCS\#11 is the most widely used
cryptographic standard of functions like signing, encryption,
decryption, \textit{etc}. API-related attacks were first discovered
in~\cite{Longley}, followed by the exposure of the vulnerability to
attacks of PKCS\#11~\cite{steel10,Clulow03onthe}. Formally analyzing
security APIs and reasoning about attacks has
been
revisited~\cite{bakproof,steelformalanalysis,steelxor,tsalapati,robbank}
through approaches like model checking; theorem proving; customized
decision procedures; or reverse-engineering for
verification~\cite{steel10,cortier,courant,steelformalanalysis,youn}.
However, security analysis has mostly focused on the RSA PKCS\#11
itself. There has been less attention given to the implementations
connected to the standard, such as the low-level communication between
the on-card and the off-card applications, defined by the Application
Data Protocol Unit (APDU).


%\begin{figure}


The basic principles of the APDU, \eg the available inter-industry
commands, the structure and contents of the exchanged messages
\textit{etc}, are specified by the ISO 7816 standard. Precisely
following the standard is not compulsory. Many smart-card
manufacturers deviate from the standard under the assumption that a
proprietary APDU implementation is more secure. REPROVE 
reverse-engineers the APDU implementation and deduces the card's
functionalities, regardless of whether it is inter-industry,
proprietary or a mixture of both.


\begin{wrapfigure}[10]{r}{0.55\linewidth}
  \vspace{-7ex}
  \centering
  \includegraphics[width=\linewidth]{systemvscard}
  \vspace{-5ex}
  \caption{High-level overview of our technique.}
  \label{cardvssystem}
%\end{figure}
\end{wrapfigure}


A high-level description of REPROVE is shown in
Figure~\ref{cardvssystem}. The card communicates with the reader and
this communication generates a trace that we reverse-engineer. The
analysis module accepts as parameters the trace and abstract models of
the cryptographic protocols; and outputs how
the card performs specific cryptographic functions. REPROVE deals with
both inter-industry and proprietary implementations. It models the
communication between a smart-card and a reader in first-order logic,
and uses reasoning and inference over knowledge bases to automatically
reverse-engineer the model. The system maintains knowledge bases of
APDU abstractions based on ISO 7816. Its reverse-engineering algorithm
parses a communication trace and uses these abstractions to draw
conclusions about the semantics of the various elements of
the trace, narrow down their possible implementations and infer the
card's actually executed operations.

\comment{To the best of our knowledge, this is the first work for
  modeling the APDU layer and formally reverse-engineering it by
  mapping the low-level communication to the on-card operations and to
  the RSA PKCS\#11 standard. The abstract models of the background
  knowledge do not hard-code the implementation. Instead, they offer a
  generic framework to automatically capture different
  implementations. Specific implementations are mapped to these
  abstractions by reasoning about the exact meaning of the low-level
  implementation. Our novelty stems from not requiring access to the
  card's software and dealing with both inter-industry and proprietary
  implementations in a single setting.}{novelty -- reviewer's comment}



%\subsection{Related Work}

%\paragraph*{Smart-card attacks}
\stitle{Smart-card attacks}
If an attacker compromises the APDU level and the
communication is not secure, she can have access
to the card's sensitive information,
\eg privacy keys, or data that should be encrypted but is not.
 \cite{Murdoch-chp-PIN}, for instance, proposes 
a man-in-the-middle device to allow authentication without knowing the
card's PIN by intercepting and modifying the
communication between the card and terminal.
%that APDUs are inter-industry, it sends a \textit{success} response to
%a \textit{verify} command that has the wrong PIN and allows
%authentication of untrustworthy parts. 
A different approach is to bypass confidentiality by assuming access to the
APDU buffer used to exchange data~\cite{barbu-eavesdropPINg-apdu-buffer}.
%In
%\cite{barbu-eavesdropPINg-apdu-buffer}, a different approach is
%adopted, where confidentiality is bypassed by assuming access to the
%APDU buffer, used to exchange
%data. 
The SmartLogic tool~\cite{smartlogig-koning} obtains full
control over the smart-card communication channel for eavesdropping
and man-in-the-middle attacks.   These
efforts % to test the vulnerabilities of smart-cards
motivate the need for a formal way of reverse-engineering the protocol  and reasoning
about smart-card security. 
A key assumption of all these approaches is that the
communication channel follows an inter-industry implementation. 
 However, a good number of smart-card vendors opt
for a proprietary implementation, which renders the existing security
analysis approaches inapplicable. A proprietary implementation of the 
communication, as witnessed by any security testing framework, looks
like a random sequence of bits that needs to be deciphered to
understand its semantics.

 
% \paragraph*{Reverse-engineering protocols}
 \comment{\stitle{Reverse-engineering protocols}}{added the suggested paper by the reviewers}
In terms of protocol
reverse-engineering, Polygot~\cite{polygot}
automatically extracts protocol messages through binary
analysis. Prospex~\cite{prospex} infers the protocol format and the
corresponding state machines.  Discoverer~\cite{discoverer} reverse-engineers 
the protocol message formats. % by the network traces, 
ReFormat~\cite{reformat} reverse-engineers encrypted messages,   \cite{cho2010} 
infers protocol state machines based
on abstractions provided by the end users. All these efforts
either:
\begin{inparaenum}
\item require software access, or
\item assume known message semantics, or
\item derive only the protocol message format without its semantics.
\end{inparaenum}
What is desirable is to make no assumptions about prior knowledge
apart from what is publically available, \ie the inter-industry
commands of ISO 7816.  
%That is, we should make no assumption of
%access to the software implementation, the format of the messages, or
%their semantics.


%\subsection{Contributions and roadmap} 

%\paragraph{Contributions and roadmap} 
\stitle{Contributions and roadmap} The main contributions of this
paper are:
\begin{compactitem}
\item Section~\ref{sec:background} gives an overview of the
  PKCS\#11 
  ISO/IEC 7816 standards.  We show the discrepancies
  between the inter-industry and proprietary definitions of
  the commands covered by the standard, and how these discrepancies
  aggravate the problem of reverse-engineering communication traces.
\item Section~\ref{methodology} \ncomment{presents the modeling of the
    APDU layer and its interconnection to PKCS\#11. Due to space
    limitations we focus on sample implementations of the
    \func{C\_logIn} function. REPROVE, however, is function-independent
    as different models can be plugged in. }{generality? ftanei afto?}
  Computing all potential proprietary implementations and testing them
  for correctness is practically infeasible, as it is a combinatorial
  problem. Instead, we produce a model that is based on decomposing the
  various functionalities of the API into finer-grained
  sub-functionalities and analyze how the commands of the standard
  can be used to implement these functionalities. %Through this
  %representation we 
  We present a reverse-engineering algorithm to
  automatically analyze a trace of commands and group them according
  to their intended functionality as this has been captured by our
  model.
%\item Section~\ref{sec:example} gives a complete example of applying
%  our algorithm on a communication trace.
\item Section~\ref{sec:evaluation} \ncomment{evaluates the accuracy 
  of  REPROVE, after automatically reverse-engineering five commercially available
  smart-cards for the  RSA
  PKCS\#11 \func{C\_logIn} function. We provide further evidence of
  REPROVE's generality by evaluating our technique on the 
   \func{C\_generateKey} function.}{generate-key: ftanei afto?}
   Our results suggest that
  our methodology can be used to automatically reverse-engineer 
  %command 
  traces to detect security flaws for
  other RSA PKCS\#11 functions as well.
\item Finally, Section~\ref{sec:conclusions} concludes the paper with
  a summary of our findings and with our future work directions.
 \end{compactitem}
 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "paperEdit"
%%% End: 
